(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const r3 Real)
(declare-const r5 Real)
(declare-const r6 Real)
(declare-const r8 Real)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const v16 Bool)
(declare-const r11 Real)
(declare-const r12 Real)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(assert (or v11 v4 (< 0.9737 478.0 r5)))
(assert (or v11 v17 v4))
(assert (or (< 0.9737 478.0 r5) v16 v17))
(assert (or v2 v12 (<= 723364.0 42920902109.0)))
(assert (or (> 42920902109.0 77.0 r3 478.0) v12 v19))
(assert (or v4 v11 (<= 36.0 r6 (/ 1841003171.0 0.8858073))))
(assert (or v16 v4 v11))
(assert (or v19 v16 v2))
(assert (or v15 v15 (<= 723364.0 42920902109.0)))
(assert (or (<= 723364.0 42920902109.0) v17 v4))
(assert (or (> 42920902109.0 77.0 r3 478.0) v15 v9))
(assert (or v2 v2 v15))
(assert (or v2 (<= r8 9738.0 0.8858073 0.9737 0.8858073) v12))
(assert (or v12 (<= r8 9738.0 0.8858073 0.9737 0.8858073) v16))
(assert (or v19 v11 v1))
(assert (or v15 v15 (> 42920902109.0 77.0 r3 478.0)))
(assert (or v2 (< 0.9737 478.0 r5) v12))
(assert (or (< 0.9737 478.0 r5) (<= 36.0 r6 (/ 1841003171.0 0.8858073)) v12))
(assert (or v12 v4 (<= (/ 1841003171.0 0.8858073) r8 r9)))
(assert (or v16 v4 v12))
(assert (or v11 v1 (<= 36.0 r6 (/ 1841003171.0 0.8858073))))
(assert (or v1 v11 (<= (/ 1841003171.0 0.8858073) r8 r9)))
(assert (or v19 v9 v17))
(assert (or (<= 36.0 r6 (/ 1841003171.0 0.8858073)) v12 (< 0.9737 478.0 r5)))
(assert (or (<= 723364.0 42920902109.0) (<= 36.0 r6 (/ 1841003171.0 0.8858073)) v16))
(assert (or (<= 36.0 r6 (/ 1841003171.0 0.8858073)) v19 v8))
(assert (or (> 42920902109.0 77.0 r3 478.0) v2 v12))
(assert (or v19 v16 (< 0.9737 478.0 r5)))
(assert (or v4 v2 v15))
(assert (or v1 (<= r8 9738.0 0.8858073 0.9737 0.8858073) (> 42920902109.0 77.0 r3 478.0)))
(assert (or v16 (< 0.9737 478.0 r5) (<= (/ 1841003171.0 0.8858073) r8 r9)))
(assert (or (<= (/ 1841003171.0 0.8858073) r8 r9) v9 v17))
(assert (or v19 (> 42920902109.0 77.0 r3 478.0) v2))
(assert (or v9 v11 v8))
(assert (or v9 v17 v9))
(assert (or v12 (> 42920902109.0 77.0 r3 478.0) v9))
(assert (or v12 v19 v19))
(assert (or v17 v9 (< 0.9737 478.0 r5)))
(assert (or v12 v17 v16))
(assert (or v8 v11 v1))
(assert (or v11 v15 v12))
(assert (or v15 v12 v11))
(assert (or v11 (<= r8 9738.0 0.8858073 0.9737 0.8858073) v11))
(assert (or v4 v1 v2))
(assert (or (<= 723364.0 42920902109.0) v2 v9))
(assert (or (< 0.9737 478.0 r5) v16 v9))
(assert (or (<= (/ 1841003171.0 0.8858073) r8 r9) v19 v1))
(assert (or (<= 36.0 r6 (/ 1841003171.0 0.8858073)) v4 (<= r8 9738.0 0.8858073 0.9737 0.8858073)))
(assert (or (<= 723364.0 42920902109.0) v19 v12))
(assert (or v4 (< 0.9737 478.0 r5) v4))
(assert (or v16 (<= 723364.0 42920902109.0) v17))
(assert (or (<= (/ 1841003171.0 0.8858073) r8 r9) v19 v1))
(assert (=> (or (<= 723364.0 42920902109.0) (<= 36.0 r6 (/ 1841003171.0 0.8858073)) v16) (or v2 v2 v15)))
(assert (or (or (<= 723364.0 42920902109.0) v17 v4) (or (< 0.9737 478.0 r5) v16 v17)))
(assert (or v11 v17 v4))
(assert (and (or (< 0.9737 478.0 r5) v16 v17) (or v19 v9 v17) (or v16 (< 0.9737 478.0 r5) (<= (/ 1841003171.0 0.8858073) r8 r9)) (or v16 (<= 723364.0 42920902109.0) v17)))
(assert (or v9 v17 v9))
(assert (or (<= 36.0 r6 (/ 1841003171.0 0.8858073)) v19 v8))
(assert (or v2 v12 (<= 723364.0 42920902109.0)))
(assert (=> (or v12 v17 v16) (or (< 0.9737 478.0 r5) v16 v17)))
(assert (or (or v16 v4 v12) (or v1 v11 (<= (/ 1841003171.0 0.8858073) r8 r9))))
(assert (and (or (or (<= 723364.0 42920902109.0) v17 v4) (or (< 0.9737 478.0 r5) v16 v17)) (or v19 v9 v17)))
(assert (=> (or v12 v17 v16) (or (< 0.9737 478.0 r5) v16 v17)))
(assert (=> (or v2 v12 (<= 723364.0 42920902109.0)) (or v12 v17 v16)))
(assert (or (or v15 v15 (> 42920902109.0 77.0 r3 478.0)) (or v11 v1 (<= 36.0 r6 (/ 1841003171.0 0.8858073)))))
(assert (or v15 v15 (<= 723364.0 42920902109.0)))
(maximize (- r3 r8))
(minimize (+ r3 r9))
(minimize (+ r3 r10))
(minimize (+ r3 r11))
(minimize (+ r3 r12))
(minimize (+ r5 r8))
(minimize (+ r5 r9))
(maximize (- r5 r10))
(minimize (+ r5 r11))
(maximize (- r5 r12))
(maximize (- r8 r9))
(maximize (- r8 r12))
(maximize (- r9 r10))
(maximize (- r10 r11))
(check-sat)
(exit)
